Nuprl Lemma : lname_wf
11,40
postcript
pdf
l
:IdLnk. lname(
l
)
Id
latex
Definitions
x
:
A
B
(
x
)
,
Id
,
t
T
,
x
.
A
(
x
)
,
x
:
A
.
B
(
x
)
,
x
.
t
(
x
)
,
t
.2
,
lname(
l
)
,
IdLnk
Lemmas
pi2
wf
,
Id
wf
origin
l:IdLnk. lname(l) 
Id l:IdLnk. lname(l) Id 
B(x) T
x.A(x)x:A. B(x)
x. t(x)